ci: wire the formal/ Coq proof gate into CI (Refs #513) - #709
Conversation
`formal/` holds 20 machine-checked Coq/Rocq proofs and `formal/justfile`
already implements a real, fail-closed check over them — but no workflow
ever invoked it, so the corpus was unchecked in CI.
Verified locally with coqc 8.20.1 before wiring: all 20 files check clean,
every `Print Assumptions` reports "Closed under the global context", and the
justfile's own assertion fires ("no axioms"). Deprecation warnings for
`app_length` only (8.18 -> 8.20 skew), no errors.
The gate is deliberately fail-closed: it does not probe for the prover and
skip when absent. The pinned container guarantees `coqc`, so a missing prover
is an infrastructure failure rather than a silent pass.
`formal/justfile` stays the single source of truth for the proof list and its
dependency order; the workflow parses that list instead of duplicating it, and
fails if any `formal/*.v` on disk is not named there — so adding a proof
without wiring it cannot go unnoticed.
Both guards were falsifier-tested locally:
- an unwired `formal/*.v` is detected and fails the run
- an `Axiom`-dependent theorem is caught by the "Axioms:" grep
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 2 resolved / 2 findingsIntegrates the Coq proof gate into CI with digest pinning and strict verification guards, but a malformed sed expression breaks proof parsing and the axiom check requires explicit Print Assumptions statements. ✅ 2 resolved✅ Bug: Malformed sed expression makes proof-list parse step always fail
✅ Edge Case: Axiom rejection only works for files containing Print Assumptions
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
1 participant
Why
formal/contains 20 machine-checked Coq/Rocq proofs, andformal/justfilealready implements a real, fail-closed check over them. No workflow ever
invoked it —
grepfor coq/rocq across.github/workflows/returned nothing,so the entire corpus was unchecked in CI.
This is the inverse of the usual fake-gate problem: the assurance already
existed and was simply being thrown away.
Verified before wiring
Ran the existing
formal/justfile checklocally withcoqc8.20.1:Print AssumptionsreportsClosed under the global context— thestrongest result, meaning no dependency on anything outside the kernel
mechanised; no axioms."
app_length, from the 8.18→8.20 skew), no errorsNote
formal/README.adocdocuments Coq/Rocq 8.18; the container here is8.20, on which the corpus was confirmed to pass.
Design
Fail-closed by construction. The gate does not probe for the prover and
skip when absent. The pinned container guarantees
coqc, so a missing prover isan infrastructure failure, not a silent pass.
No duplicated proof list.
formal/justfilestays the single source of truthfor the list and its dependency order; the workflow parses it rather than
re-stating it. A completeness guard fails the run if any
formal/*.von disk isnot named there — so adding a proof without wiring it cannot silently go
unchecked.
Falsifier-tested
Both guards were proven to actually fire, not merely to pass:
formal/ZZ_Falsifier.vAxiom cheatPrint AssumptionsemitsAxioms:, grep catches it, run failsNotes
coqorg/coq@sha256:e50d77c4…)actions/checkoutSHA-pinned to match repo conventionpermissions:at column 0, perworkflow-linter.ymltimeout-minutes: 30Draft — this is the first time these proofs will run in CI.
🤖 Generated with Claude Code